#pragma once
#include "PDTExpNumSing.h"
#include "PDTVar.h"
#include "PDTNumConst.h"
#include "PDTCodeGraph.h"

class PDTQuantifier;
class PDTIntRange;

class PDTNumVar  :  public PDTExpNumSing, public PDTVar, public TraverseIfc <PDTNumVar , PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTNumVar )
public:
  PDTNumVar(PDTCodeGraph & CG, string name, PDTQuantifier * aq = NULL, PDTIntRange * aRange = NULL);

  NodeTypeEnum
  getType()
  {
    return PDTNumVar_Em;
  }

  virtual PDTNode*
  getNode()
  {
    return this;
  }

  virtual void
  printType()
  {
    cout << "PDTNumVar_Em";
  }

  bool
  isNumVar()
  {
    return true;
  }

  bool
  isVar()
  {
    return true;
  }

  virtual
  ~PDTNumVar()
  {
  }
	virtual bool eval(PDTCodeGraph &CG)
	{
		if (nValue == NULL)
		{
			cout<<"Variable '"<<getName()<<"' is not assigned yet"<<endl;
			return true;
		}
		else
		{
			cout<<"Variable '"<<getName()<<"' has the numeric value "<<(dynamic_cast<PDTNumConstInt*>(nValue))->getValue()<<endl;
			return true;
		}
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		stringstream sss;
		sss<<cloneID;
		if (!touched) //if not already cloned
		{
			PDTNode* toReturn;
			toReturn = new PDTNumVar(CG, getName()+"!"+sss.str(),NULL,NULL);
			cout<<"NEW VARIABLE CREATED: "<<getName()+"!"+sss.str()<<endl;
			touched = true;
			return toReturn;
		}
		else
		{
			PDTNode* existClone = CG.findVariable(getName()+"!"+sss.str());
			return existClone;
		}
	}


  virtual stringstream &
  toString(stringstream & ss) const
  {
    ss << getName();
    return ss;
  }

virtual PDTNode* getValue(){
	return nValue;
}

  virtual Z3_ast
  Z3NodeVisit (PDTZ3Visitor &ZV);
  virtual Z3_ast
  Z3value(PDTZ3Visitor &ZV);
  virtual bool SMT2visit(PDTSMT2Visitor & );
};
